Don't hassle me about emacs.texi.

diff --git a/make-dist b/make-dist
index b95156b9aa2b67d8743a005bc8e572a88909f4d1..fb54f597589d1cf62b80a9d9023bc20db4c94ad4 100755 (executable)
--- a/make-dist
+++ b/make-dist
@@ -73,7 +73,7 @@ if grep -s "GNU Emacs version ${version}" ./man/emacs.texi > /dev/null; then
   true
 else
   echo "You must update the version number in \`./man/emacs.texi'"
-  exit 1
+  sleep 5
 fi
 
 ### Make sure the subdirectory is available.